st-key-match(tab;k1;k2)
== case k1
== of inl(n) => case k2
== of inl(n) => of inl(m) => ff
== of inl(n) => o| inr(a) => (n <z ptr(tab)  n <z ||tab|| )  st-atom(tab;n) =a1 a
== o| inr(a) => case k2
== o| inr(a) => of inl(n) => (n <z ptr(tab)  n <z ||tab|| )  st-atom(tab;n) =a1 a
== o| inr(a) => o| inr(b) => ff 

latex

---

clarification:

st-key-match(tab;k1;k2)
== case k1
== of inl(n) => case k2
== of inl(n) => of inl(m) => ff
== of inl(n) => o| inr(a) => (n <z ptr(tab)  n <z ||tab|| )  eq_atom1(st-atom(tab;n);a)
== o| inr(a) => case k2
== o| inr(a) => of inl(n) => (n <z ptr(tab)  n <z ||tab|| )  eq_atom1(st-atom(tab;n);a)
== o| inr(a) => o| inr(b) => ff 

latex

Definitions	case b of inl(x) => s(x) | inr(y) => t(y), p  q, ptr(tab), i <z j, ||tab|| , eq_atom$n(x;y), st-atom(tab;n), ff
FDL editor aliases	st-key-match